(set-info :source |fuzzsmt|)
(set-info :smt-lib-version 2.0)
(set-info :category "random")
(set-info :status unknown)
(set-logic QF_LIA)
(declare-fun v0 () Int)
(assert (let ((e1 1))
(let ((e2 4))
(let ((e3 0))
(let ((e4 (- v0)))
(let ((e5 (+ e4 e4)))
(let ((e6 (+ e4 e5)))
(let ((e7 (* e3 e5)))
(let ((e8 (+ e7 e4)))
(let ((e9 (+ e7 e5)))
(let ((e10 (- e9)))
(let ((e11 (* e2 e9)))
(let ((e12 (- e9 e8)))
(let ((e13 (* e3 e4)))
(let ((e14 (- e9 e11)))
(let ((e15 (- e14 e5)))
(let ((e16 (- v0 e12)))
(let ((e17 (+ e12 e12)))
(let ((e18 (+ e15 e12)))
(let ((e19 (* e15 e2)))
(let ((e20 (- e4)))
(let ((e21 (- e4 e6)))
(let ((e22 (+ e8 e18)))
(let ((e23 (- e16 e9)))
(let ((e24 (- e20)))
(let ((e25 (- e10 e12)))
(let ((e26 (+ e6 e8)))
(let ((e27 (* e1 e12)))
(let ((e28 (<= e6 e25)))
(let ((e29 (< e11 e15)))
(let ((e30 (= e17 e18)))
(let ((e31 (> e13 e9)))
(let ((e32 (= e19 e17)))
(let ((e33 (> e13 e17)))
(let ((e34 (= e5 e27)))
(let ((e35 (distinct e27 v0)))
(let ((e36 (<= e24 e26)))
(let ((e37 (< e25 e16)))
(let ((e38 (> e27 e20)))
(let ((e39 (distinct e13 e6)))
(let ((e40 (= e9 e9)))
(let ((e41 (<= e23 e7)))
(let ((e42 (>= e7 v0)))
(let ((e43 (= e17 e16)))
(let ((e44 (<= e25 v0)))
(let ((e45 (>= e12 e11)))
(let ((e46 (> e26 e25)))
(let ((e47 (> e11 e20)))
(let ((e48 (< e18 e18)))
(let ((e49 (distinct e16 e8)))
(let ((e50 (>= e16 e24)))
(let ((e51 (> v0 e10)))
(let ((e52 (distinct e27 e14)))
(let ((e53 (= e22 e26)))
(let ((e54 (distinct e9 e21)))
(let ((e55 (<= e18 e17)))
(let ((e56 (distinct e22 e23)))
(let ((e57 (>= e26 e14)))
(let ((e58 (= e19 e7)))
(let ((e59 (distinct e18 e14)))
(let ((e60 (> e20 e5)))
(let ((e61 (> e14 e25)))
(let ((e62 (distinct e16 e4)))
(let ((e63 (ite e39 e21 e27)))
(let ((e64 (ite e52 e22 e22)))
(let ((e65 (ite e43 e10 e15)))
(let ((e66 (ite e35 e15 e24)))
(let ((e67 (ite e46 e17 e25)))
(let ((e68 (ite e50 e64 e11)))
(let ((e69 (ite e38 e5 e22)))
(let ((e70 (ite e55 e68 e15)))
(let ((e71 (ite e52 e14 e7)))
(let ((e72 (ite e41 e8 e22)))
(let ((e73 (ite e57 e16 e71)))
(let ((e74 (ite e50 e26 e10)))
(let ((e75 (ite e46 e14 e14)))
(let ((e76 (ite e32 e19 e24)))
(let ((e77 (ite e47 e6 e63)))
(let ((e78 (ite e61 e11 e8)))
(let ((e79 (ite e48 e18 e73)))
(let ((e80 (ite e59 e20 e6)))
(let ((e81 (ite e58 e77 e26)))
(let ((e82 (ite e42 e11 e75)))
(let ((e83 (ite e54 e68 e15)))
(let ((e84 (ite e60 e23 e23)))
(let ((e85 (ite e46 v0 e11)))
(let ((e86 (ite e40 e13 e14)))
(let ((e87 (ite e55 e22 e66)))
(let ((e88 (ite e51 e4 e20)))
(let ((e89 (ite e41 e9 e6)))
(let ((e90 (ite e55 e12 e74)))
(let ((e91 (ite e36 e26 e80)))
(let ((e92 (ite e48 e19 e24)))
(let ((e93 (ite e34 e85 e14)))
(let ((e94 (ite e57 e80 e87)))
(let ((e95 (ite e56 e94 e14)))
(let ((e96 (ite e29 e15 e8)))
(let ((e97 (ite e31 e9 e92)))
(let ((e98 (ite e28 e80 e16)))
(let ((e99 (ite e61 e70 e7)))
(let ((e100 (ite e44 e76 e9)))
(let ((e101 (ite e38 e76 e92)))
(let ((e102 (ite e62 e86 e13)))
(let ((e103 (ite e33 e100 e73)))
(let ((e104 (ite e32 e18 e25)))
(let ((e105 (ite e30 e79 e7)))
(let ((e106 (ite e53 e103 e64)))
(let ((e107 (ite e43 e24 e16)))
(let ((e108 (ite e37 e66 e11)))
(let ((e109 (ite e49 e106 e72)))
(let ((e110 (ite e45 e73 e74)))
(let ((e111 (> e70 e87)))
(let ((e112 (>= e22 e90)))
(let ((e113 (>= e75 e26)))
(let ((e114 (= e4 e85)))
(let ((e115 (distinct e103 e107)))
(let ((e116 (> e16 e93)))
(let ((e117 (<= e81 e8)))
(let ((e118 (> e13 e27)))
(let ((e119 (distinct e98 e25)))
(let ((e120 (<= e92 e76)))
(let ((e121 (> e65 e100)))
(let ((e122 (<= e64 e91)))
(let ((e123 (= e14 e8)))
(let ((e124 (< e82 e84)))
(let ((e125 (> e89 e4)))
(let ((e126 (> e99 e7)))
(let ((e127 (= e70 e83)))
(let ((e128 (< e93 e101)))
(let ((e129 (> e87 e86)))
(let ((e130 (= e83 e12)))
(let ((e131 (> e94 e76)))
(let ((e132 (>= e105 e83)))
(let ((e133 (distinct e96 e108)))
(let ((e134 (<= e79 e21)))
(let ((e135 (distinct e19 e8)))
(let ((e136 (<= e12 e97)))
(let ((e137 (<= e106 e7)))
(let ((e138 (<= e100 e13)))
(let ((e139 (> e85 e18)))
(let ((e140 (> e78 e75)))
(let ((e141 (= e107 e72)))
(let ((e142 (>= e19 e70)))
(let ((e143 (distinct e18 e81)))
(let ((e144 (< e93 e14)))
(let ((e145 (< e102 e94)))
(let ((e146 (>= v0 e91)))
(let ((e147 (> v0 e74)))
(let ((e148 (distinct e65 e93)))
(let ((e149 (>= e73 e100)))
(let ((e150 (= e25 e86)))
(let ((e151 (<= e16 e26)))
(let ((e152 (< e99 e5)))
(let ((e153 (< e88 e6)))
(let ((e154 (< e68 e82)))
(let ((e155 (= e106 e83)))
(let ((e156 (distinct e96 e83)))
(let ((e157 (<= e78 e70)))
(let ((e158 (= e105 e91)))
(let ((e159 (distinct e7 e75)))
(let ((e160 (distinct e90 e78)))
(let ((e161 (< e102 e109)))
(let ((e162 (< e78 e12)))
(let ((e163 (> e11 e65)))
(let ((e164 (> e97 e94)))
(let ((e165 (= e20 v0)))
(let ((e166 (>= e27 e87)))
(let ((e167 (> e85 e108)))
(let ((e168 (> e18 e98)))
(let ((e169 (< e98 e23)))
(let ((e170 (= e87 e20)))
(let ((e171 (distinct e67 e13)))
(let ((e172 (>= v0 e77)))
(let ((e173 (>= v0 e108)))
(let ((e174 (= e76 e110)))
(let ((e175 (distinct e97 e8)))
(let ((e176 (>= e16 e87)))
(let ((e177 (< e9 e16)))
(let ((e178 (> e95 e89)))
(let ((e179 (distinct e86 e8)))
(let ((e180 (<= e108 e91)))
(let ((e181 (distinct e10 e106)))
(let ((e182 (< e92 e27)))
(let ((e183 (> e108 e63)))
(let ((e184 (<= e84 e75)))
(let ((e185 (= e71 e96)))
(let ((e186 (<= e94 e63)))
(let ((e187 (distinct e93 e20)))
(let ((e188 (>= e89 e8)))
(let ((e189 (>= e4 e11)))
(let ((e190 (distinct e90 e89)))
(let ((e191 (= e92 e89)))
(let ((e192 (<= e82 e73)))
(let ((e193 (distinct e17 e80)))
(let ((e194 (< e92 e85)))
(let ((e195 (= e6 e104)))
(let ((e196 (distinct e10 e88)))
(let ((e197 (distinct e110 e108)))
(let ((e198 (< e17 v0)))
(let ((e199 (> e5 e110)))
(let ((e200 (distinct e19 e5)))
(let ((e201 (<= e93 e91)))
(let ((e202 (<= e10 e96)))
(let ((e203 (= e74 e23)))
(let ((e204 (distinct e4 e106)))
(let ((e205 (= e95 e74)))
(let ((e206 (distinct e95 e81)))
(let ((e207 (<= e81 e88)))
(let ((e208 (< e92 e90)))
(let ((e209 (<= e66 e81)))
(let ((e210 (> e10 e4)))
(let ((e211 (= e87 e25)))
(let ((e212 (>= e107 e71)))
(let ((e213 (>= e103 e91)))
(let ((e214 (> e19 e97)))
(let ((e215 (<= e95 e81)))
(let ((e216 (>= e65 e15)))
(let ((e217 (< e75 e102)))
(let ((e218 (distinct e75 e110)))
(let ((e219 (= e20 e79)))
(let ((e220 (distinct e13 e107)))
(let ((e221 (distinct e9 e77)))
(let ((e222 (< e22 e67)))
(let ((e223 (distinct e21 e109)))
(let ((e224 (> e82 e69)))
(let ((e225 (distinct e80 e101)))
(let ((e226 (= v0 e64)))
(let ((e227 (= e77 e17)))
(let ((e228 (<= e101 e85)))
(let ((e229 (distinct e102 e82)))
(let ((e230 (= e10 e105)))
(let ((e231 (= e81 e72)))
(let ((e232 (>= e109 e14)))
(let ((e233 (>= e13 e91)))
(let ((e234 (< e26 e84)))
(let ((e235 (= e11 e95)))
(let ((e236 (<= e73 e12)))
(let ((e237 (distinct e101 e20)))
(let ((e238 (>= e67 e97)))
(let ((e239 (= e103 e7)))
(let ((e240 (> e83 e11)))
(let ((e241 (= e86 e20)))
(let ((e242 (<= e109 e99)))
(let ((e243 (>= e12 e93)))
(let ((e244 (distinct e18 e65)))
(let ((e245 (distinct e65 e21)))
(let ((e246 (> e89 e80)))
(let ((e247 (> e67 e82)))
(let ((e248 (> e82 e82)))
(let ((e249 (< e82 e21)))
(let ((e250 (< e11 e84)))
(let ((e251 (> e77 e6)))
(let ((e252 (< e103 e12)))
(let ((e253 (>= e97 e102)))
(let ((e254 (= e8 e25)))
(let ((e255 (<= e4 e26)))
(let ((e256 (< e79 e23)))
(let ((e257 (distinct e24 e76)))
(let ((e258 (ite e129 e57 e154)))
(let ((e259 (and e130 e221)))
(let ((e260 (or e123 e239)))
(let ((e261 (xor e249 e127)))
(let ((e262 (= e202 e166)))
(let ((e263 (and e114 e199)))
(let ((e264 (= e198 e224)))
(let ((e265 (= e170 e207)))
(let ((e266 (xor e208 e203)))
(let ((e267 (or e52 e257)))
(let ((e268 (=> e126 e135)))
(let ((e269 (and e41 e56)))
(let ((e270 (xor e241 e36)))
(let ((e271 (xor e160 e131)))
(let ((e272 (and e31 e244)))
(let ((e273 (xor e112 e138)))
(let ((e274 (= e211 e201)))
(let ((e275 (not e186)))
(let ((e276 (or e222 e210)))
(let ((e277 (=> e180 e269)))
(let ((e278 (and e267 e251)))
(let ((e279 (not e147)))
(let ((e280 (ite e264 e174 e149)))
(let ((e281 (not e254)))
(let ((e282 (or e59 e59)))
(let ((e283 (xor e252 e146)))
(let ((e284 (= e128 e228)))
(let ((e285 (or e155 e152)))
(let ((e286 (xor e145 e39)))
(let ((e287 (or e116 e280)))
(let ((e288 (xor e232 e263)))
(let ((e289 (and e216 e167)))
(let ((e290 (and e217 e256)))
(let ((e291 (and e289 e259)))
(let ((e292 (ite e162 e44 e62)))
(let ((e293 (and e270 e137)))
(let ((e294 (=> e181 e231)))
(let ((e295 (not e204)))
(let ((e296 (= e122 e229)))
(let ((e297 (not e192)))
(let ((e298 (and e200 e220)))
(let ((e299 (ite e183 e42 e218)))
(let ((e300 (=> e136 e51)))
(let ((e301 (or e49 e173)))
(let ((e302 (not e291)))
(let ((e303 (and e159 e283)))
(let ((e304 (and e184 e58)))
(let ((e305 (= e60 e260)))
(let ((e306 (and e150 e236)))
(let ((e307 (=> e212 e246)))
(let ((e308 (not e151)))
(let ((e309 (=> e304 e297)))
(let ((e310 (not e225)))
(let ((e311 (and e142 e133)))
(let ((e312 (and e311 e298)))
(let ((e313 (not e303)))
(let ((e314 (or e143 e144)))
(let ((e315 (or e307 e205)))
(let ((e316 (and e55 e40)))
(let ((e317 (and e134 e195)))
(let ((e318 (ite e169 e28 e238)))
(let ((e319 (= e245 e29)))
(let ((e320 (ite e243 e227 e156)))
(let ((e321 (= e125 e115)))
(let ((e322 (and e47 e305)))
(let ((e323 (xor e168 e287)))
(let ((e324 (xor e284 e290)))
(let ((e325 (= e301 e293)))
(let ((e326 (or e30 e288)))
(let ((e327 (xor e271 e240)))
(let ((e328 (xor e296 e48)))
(let ((e329 (or e310 e193)))
(let ((e330 (xor e171 e132)))
(let ((e331 (ite e276 e302 e330)))
(let ((e332 (xor e281 e219)))
(let ((e333 (= e120 e272)))
(let ((e334 (xor e185 e292)))
(let ((e335 (=> e139 e178)))
(let ((e336 (not e213)))
(let ((e337 (not e175)))
(let ((e338 (=> e285 e334)))
(let ((e339 (or e161 e118)))
(let ((e340 (= e157 e268)))
(let ((e341 (ite e191 e189 e319)))
(let ((e342 (or e338 e61)))
(let ((e343 (not e317)))
(let ((e344 (or e329 e277)))
(let ((e345 (ite e320 e279 e309)))
(let ((e346 (not e282)))
(let ((e347 (= e332 e318)))
(let ((e348 (and e340 e278)))
(let ((e349 (and e321 e187)))
(let ((e350 (or e164 e196)))
(let ((e351 (=> e215 e344)))
(let ((e352 (ite e336 e113 e265)))
(let ((e353 (=> e37 e33)))
(let ((e354 (or e349 e153)))
(let ((e355 (or e273 e250)))
(let ((e356 (and e163 e314)))
(let ((e357 (=> e46 e335)))
(let ((e358 (= e172 e194)))
(let ((e359 (=> e351 e348)))
(let ((e360 (ite e117 e266 e50)))
(let ((e361 (=> e357 e300)))
(let ((e362 (= e165 e141)))
(let ((e363 (not e312)))
(let ((e364 (=> e275 e341)))
(let ((e365 (=> e343 e345)))
(let ((e366 (=> e214 e53)))
(let ((e367 (xor e364 e230)))
(let ((e368 (= e54 e45)))
(let ((e369 (ite e356 e209 e352)))
(let ((e370 (= e258 e360)))
(let ((e371 (and e188 e315)))
(let ((e372 (and e361 e294)))
(let ((e373 (= e247 e350)))
(let ((e374 (ite e355 e34 e177)))
(let ((e375 (or e372 e367)))
(let ((e376 (not e286)))
(let ((e377 (= e365 e354)))
(let ((e378 (xor e353 e377)))
(let ((e379 (not e374)))
(let ((e380 (= e323 e378)))
(let ((e381 (=> e371 e308)))
(let ((e382 (xor e148 e248)))
(let ((e383 (not e331)))
(let ((e384 (=> e366 e358)))
(let ((e385 (or e226 e325)))
(let ((e386 (xor e379 e369)))
(let ((e387 (or e380 e35)))
(let ((e388 (=> e140 e387)))
(let ((e389 (xor e385 e326)))
(let ((e390 (and e362 e235)))
(let ((e391 (=> e190 e262)))
(let ((e392 (or e306 e261)))
(let ((e393 (=> e388 e327)))
(let ((e394 (ite e299 e179 e324)))
(let ((e395 (ite e32 e337 e347)))
(let ((e396 (and e391 e121)))
(let ((e397 (= e383 e333)))
(let ((e398 (xor e363 e242)))
(let ((e399 (xor e158 e390)))
(let ((e400 (xor e373 e373)))
(let ((e401 (= e346 e368)))
(let ((e402 (not e182)))
(let ((e403 (and e124 e295)))
(let ((e404 (ite e403 e386 e119)))
(let ((e405 (and e359 e233)))
(let ((e406 (ite e381 e322 e393)))
(let ((e407 (ite e384 e328 e395)))
(let ((e408 (and e237 e274)))
(let ((e409 (= e176 e396)))
(let ((e410 (xor e407 e38)))
(let ((e411 (or e223 e402)))
(let ((e412 (not e313)))
(let ((e413 (or e255 e206)))
(let ((e414 (=> e397 e397)))
(let ((e415 (and e409 e404)))
(let ((e416 (xor e111 e339)))
(let ((e417 (xor e376 e414)))
(let ((e418 (or e410 e394)))
(let ((e419 (not e400)))
(let ((e420 (and e408 e253)))
(let ((e421 (= e389 e416)))
(let ((e422 (ite e421 e412 e412)))
(let ((e423 (ite e399 e420 e413)))
(let ((e424 (ite e234 e398 e422)))
(let ((e425 (xor e392 e342)))
(let ((e426 (or e417 e401)))
(let ((e427 (=> e415 e375)))
(let ((e428 (=> e425 e427)))
(let ((e429 (=> e419 e424)))
(let ((e430 (or e316 e426)))
(let ((e431 (xor e430 e405)))
(let ((e432 (or e418 e411)))
(let ((e433 (=> e406 e431)))
(let ((e434 (or e429 e423)))
(let ((e435 (or e434 e428)))
(let ((e436 (or e382 e382)))
(let ((e437 (xor e433 e435)))
(let ((e438 (ite e43 e197 e370)))
(let ((e439 (or e432 e437)))
(let ((e440 (not e438)))
(let ((e441 (or e440 e436)))
(let ((e442 (not e441)))
(let ((e443 (= e439 e442)))
e443
))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))

(check-sat)
